$\forall$${\it es}$:ES, ${\it Cmd}$:Type, ${\it isupdate}$:(${\it Cmd}$$\rightarrow\mathbb{B}$), ${\it In}$:AbsInterface(${\it Cmd}$), ${\it Sys}$:AbsInterface(Top).
\\[0ex](E(${\it In}$) $\subseteq$r E(${\it Sys}$))
\\[0ex]$\Rightarrow$ ($\forall$$f$:sys{-}antecedent(${\it es}$;${\it Sys}$), $a$:E(${\it Sys}$). should{-}forward(${\it es}$; ${\it In}$; ${\it isupdate}$; $f$; $a$) $\in$ $\mathbb{P}$)